\begin{tabbing}
frame{-}p(${\it es}$; $i$; $T$; $x$; $L$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=subtype\_rel(es{-}vartype(${\it es}$; $i$; $x$); $T$)\+
\\[0ex]c$\wedge$ alle{-}at(\=${\it es}$;\+
\\[0ex]$i$;
\\[0ex]$e$.(($\neg$(es{-}kind(${\it es}$; $e$) $\in$ $L$))
\\[0ex]$\Rightarrow$ ($\forall$$t$:rationals. es\_state\_after(${\it es}$; $e$)($x$,$t$) = es\_state\_when(${\it es}$; $e$)($x$,$t$)))
\\[0ex])
\-\-
\end{tabbing}